Nuprl Lemma : es-decl_wf
11,40
postcript
pdf
es
:ES,
ds
:(Id
Type),
da
:(Id
Knd
Type). es-decl(
es
;
ds
;
da
)
latex
Definitions
ES
,
t
T
,
Type
,
Id
,
x
:
A
B
(
x
)
,
Knd
,
f
(
a
)
,
x
:
A
.
B
(
x
)
,
kindtype(
i
;
k
)
,
hasloc(
k
;
i
)
,
b
,
,
P
Q
,
state@
i
,
x
:
A
B
(
x
)
,
P
&
Q
,
es-decl(
es
;
ds
;
da
)
Lemmas
es-state
wf
,
assert
wf
,
hasloc
wf
,
subtype
rel
wf
,
es-kindtype
wf
,
Knd
wf
,
Id
wf
,
event
system
wf
origin
es:ES, ds:(Id
Type), da:(IdKndType). es-decl(es;ds;da) 
es:ES, ds:(IdType), da:(IdKndType). es-decl(es;ds;da) TB(x)x:A. B(x)
b
Q
B(x)